D:Dsys.
Feasible(D)
 (v:(i:IdM(i).state), sched:(Id((IdLnk+Id)+Unit)),
 (dec:(i,a:IdM(i).state(M(i).da(locl(a))+Unit)).
 (d-comp(D;v;sched;dec)  t:(t(i:Idd-world-state(D;i)))(i:Idd-world-state(D;i))) 

latex

Definitions	t  T, x:A. B(x), P  Q, Feasible(D), P & Q, M.dout2(l;tg)
Lemmas	dsys wf, d-feasible wf, d-comp wf, Id wf, IdLnk wf